We provide a formal proof on the correctness of NegaScout, which cannot be found in other places of Web.
We also find that we can also perform the scout step even for the first child of a node. It means that the constraint on the “first action” (see Line 6 of the algorithm in the pdf) is NOT necessary. It is only necessary when $\alpha = -\infty $.
Please check the following pdf.
(Thanks to Rongqing Wang.)